/*
 * ARF.cc
 *
 *  Created on:
 *      Author: catching
 */
#include "ARF.h"
#include <string>
#include <stdlib.h>
#include <fstream>
using namespace std;

#define Dir_werePrincess string("/home/catching/workspace/new_project/princess-bin-2011-07-15/werePrincess")
Prop* Prop_Append(Prop *, LogicType, Prop *);//append Prop
Prop* Neg_Prop(Prop*);
bool Trace_Back(ART_NODE*);
string Prop_to_String(Prop* p);
void Abstration(ART_NODE*);

bool CompareExpr(Expr*, Expr*);

extern int exp(int x, int t);
extern string Int2String(int y);
extern string Expr2String(Expr* e);

int n_node;//for debug
ART_NODE::ART_NODE(ART_NODE* p, Node* c){
	Parent = p;
	cfa_node = c;
	phi = cphi = NULL;
	traveled = false;
	//cout<<endl<<"New Node "<<n_node<<":Parent="<<Parent<<" cfa_node="<<cfa_node<<endl;
	node_id = n_node;
	n_node++;

	//if(typeid(*c) == typeid(UniNode)){
	//	cout<<"statement:"<<((UniNode*)c)->statement<<endl;
	//}
	//else if(typeid(*c) == typeid(BinNode)){
	//	cout<<"statement:"<<((BinNode*)c)->statement<<endl;
	//}

	return ;
}

ART_NODE* ART_NODE::ADD_CHILD(ART_NODE* temp){
	CHILD_list.insert(temp);
	return temp;
}

void ART_NODE::CLEAR_CHILD(){
	CHILD_list.clear();
	return;
}

int ART_NODE::nCHILD(){
	return CHILD_list.size();
}

bool ART_NODE::set_traveled(bool i){
	traveled = i;
	return traveled;
}

bool ART_NODE::is_traveled(){
	set<ART_NODE*>::iterator i;
	if(traveled == true){//if this node is traveled
		return traveled;
	}
	else if(CHILD_list.size() == 0){//if this node has no child
		if(typeid(*this) == typeid(BadNode)){//this is a terminal node
			return set_traveled(true);
		}
		else{//this is not a terminal node
			return set_traveled(false);
		}
	}
	else{//is this node has any child
		for(i=CHILD_list.begin(); i != CHILD_list.end(); i++){
			if((*i)->is_traveled() == false)
				return set_traveled(false);
		}
		return set_traveled(true);
	}
}

bool ARF::is_Covered(ART_NODE* t){//if there is a node cover this node, it will return true otherwise false
	ART_NODE* ART_root=t;
	while(ART_root->Parent != NULL){
		ART_root = ART_root->Parent;
	}

	if(cover_map.count(ART_root)){//if the node is in map
		if(cover_map[ART_root].count(t->cfa_node)){//if the node is in map

			set<ART_NODE*>::iterator it = cover_map[ART_root][t->cfa_node]->begin();
			set<ART_NODE*>::iterator it_end = cover_map[ART_root][t->cfa_node]->end();
			Prop* temp_prop = (*it)->phi;
			++it;

			while(it!=it_end){
				//BoolProp, NegProp, BinProp, InequProp
				temp_prop = Prop_Append(temp_prop, Or, (*it)->phi);
				++it;
			}
			bool result = interfaceSMT(Prop_Append(Neg_Prop(temp_prop), And, t->phi));
			cover_map[ART_root][t->cfa_node]->insert(t);
			cout<<"cover map: art NODE"<<t->get_node_id()<<" cfa->"<<t->cfa_node<<" prop:"<<Prop_to_String(t->phi)<<endl;
			return result;
		}
		else{//if the node is not in the map
			cout<<"not covered by others"<<endl;
			set<ART_NODE*>* temp_set = new set<ART_NODE*>;
			temp_set->insert(t);
			cover_map[ART_root].insert(pair<Node*, set<ART_NODE*>*>(t->cfa_node, temp_set));
			return false;
		}
	}
	else{//if the node is not in the map
		cout<<"not covered by others"<<endl;
		set<ART_NODE*>* temp_set = new set<ART_NODE*>;
		temp_set->insert(t);
		map<Node*, set<ART_NODE*>*> map_temp;
		map_temp.insert(pair<Node*, set<ART_NODE*>*>(t->cfa_node, temp_set));
		cover_map.insert(pair<ART_NODE*, map<Node*, set<ART_NODE*>*> >(ART_root, map_temp));
		return false;
	}
	/*
	if(cover_map.count(t->cfa_node)){//if the node is in map
		cout<<"cover map: cfa->"<<t->cfa_node<<" prop:"<<Prop_to_String(t->phi)<<endl;
		set<Prop*>::iterator it = cover_map[t->cfa_node]->begin();
		set<Prop*>::iterator it_end = cover_map[t->cfa_node]->end();
		Prop* temp_prop = *it;
		++it;

		while(it!=it_end){
			//BoolProp, NegProp, BinProp, InequProp
			temp_prop = Prop_Append(temp_prop, Or, *it);
			++it;
		}
		cover_map[t->cfa_node]->insert(t->phi);
		return interfaceSMT(Prop_Append(Neg_Prop(temp_prop), And, t->phi));
	}
	else{//if the node is not in the map
		cout<<"not covered by others"<<endl;
		set<Prop*>* temp_set = new set<Prop*>;
		temp_set->insert(t->phi);
		cover_map.insert(pair<Node*, set<Prop*>*>(t->cfa_node, temp_set));
		return false;
	}
	*/

}

bool ARF::is_Covered(string function_name, ART_NODE* t, ART_NODE* artnode_temp){
	vector<summary_edge>::iterator it_se = summary_edge_set.begin();
	vector<summary_edge>::iterator it_se_end = summary_edge_set.end();
	while(it_se != it_se_end){
		if(it_se->function_name == function_name){
			if(is_equal(it_se->root, t)){
				caller_tree_table.push_back(caller_tree(artnode_temp, it_se->root, t->cphi));
				cout<<"NODE "<<t->get_node_id()<<" function covered by NODE "<<it_se->root->get_node_id()<<endl;
				return true;
			}
		}
		it_se++;
	}
	caller_tree_table.push_back(caller_tree(artnode_temp, t, t->cphi));
	return false;
}

void ARF::Remove_from_Covermap(ART_NODE* t){
	map<ART_NODE*, map<Node*, set<ART_NODE*>*> >::iterator it_map = cover_map.begin();
	map<ART_NODE*, map<Node*, set<ART_NODE*>*> >::iterator it_map_end = cover_map.end();
	while(it_map != it_map_end){
		map<Node*, set<ART_NODE*>*>::iterator it_map_second = it_map->second.begin();
		map<Node*, set<ART_NODE*>*>::iterator it_map_second_end = it_map->second.end();
		while(it_map_second != it_map_second_end){
			set<ART_NODE*>::iterator it_map_third = it_map_second->second->begin();
			set<ART_NODE*>::iterator it_map_third_end = it_map_second->second->end();
			while(it_map_third != it_map_third_end){
				if(*it_map_third == t){
					it_map_second->second->erase(it_map_third);
					cout<<"Remove NODE "<<t->get_node_id()<<" from cover map."<<endl;
					if(it_map_second->second->empty())
						it_map->second.erase(it_map_second);
					if(it_map->second.empty())
						cover_map.erase(it_map);
					return ;
				}
				it_map_third++;
			}
			it_map_second++;
		}
		it_map++;
	}
	return ;
}

void ARF::Remove_from_processing_node(ART_NODE* t){
	stack<ART_NODE*> stack2;
	while(!processing_node.empty()){
		if(processing_node.top() != t)
			stack2.push(processing_node.top());
		else
			cout<<"Remove Node "<<t->get_node_id()<<" from stack processing node."<<endl;
		processing_node.pop();
	}
	while(!stack2.empty()){
		processing_node.push(stack2.top());
		stack2.pop();
	}
	return ;
}

void ART_NODE::DELETE_CHILD(ART_NODE* t){
	this->CHILD_list.erase(t);
	return ;
}

Expr* ARF::copy_expr(Expr* e){
	//1.IntExpr, 2.SelectExpr, 3:VarExpr, 4:BinExpr, 5:StoreExpr
	if(typeid(*e) == typeid(IntExpr)){
		IntExpr* _e = new IntExpr;
		_e->i = ((IntExpr*)e)->i;
		return _e;
	}
	else if(typeid(*e) == typeid(SelectExpr)){
		SelectExpr* _e = new SelectExpr;
		_e->a = copy_expr(((SelectExpr*)e)->a);
		_e->i = copy_expr(((SelectExpr*)e)->i);
		return _e;
	}
	else if(typeid(*e) == typeid(VarExpr)){
		VarExpr* _e = new VarExpr;
		strcpy(_e->x, ((VarExpr*)e)->x);
		return _e;
	}
	else if(typeid(*e) == typeid(BinExpr)){
		BinExpr* _e = new BinExpr;
		_e->e1 = copy_expr(((BinExpr*)e)->e1);
		_e->e2 = copy_expr(((BinExpr*)e)->e2);
		_e->op = ((BinExpr*)e)->op;
		return _e;
	}
	else if(typeid(*e) == typeid(StoreExpr)){
		StoreExpr* _e = new StoreExpr;
		_e->a = copy_expr(((StoreExpr*)e)->a);
		_e->e = copy_expr(((StoreExpr*)e)->e);
		_e->i = copy_expr(((StoreExpr*)e)->i);
		return _e;
	}
	else {
		cout<<"error when copy expr."<<endl;
		exit(1);
	}
	return NULL;
}

Prop* ARF::copy_prop(Prop* p){
	if(typeid(*p) == typeid(BoolProp)){
		BoolProp* _p = new BoolProp;
		_p->b = ((BoolProp*)p)->b;
		return _p;
	}
	else if(typeid(*p) == typeid(NegProp)){
		NegProp* _p = new NegProp;
		_p->p = copy_prop(((NegProp*)p)->p);
		return _p;
	}
	else if(typeid(*p) == typeid(BinProp)){
		BinProp* _p = new BinProp;
		_p->p1 = copy_prop(((BinProp*)p)->p1);
		_p->p2 = copy_prop(((BinProp*)p)->p2);
		_p->l = ((BinProp*)p)->l;
		return _p;
	}
	else if(typeid(*p) == typeid(InequProp)){
		InequProp* _p = new InequProp;
		_p->e1 = copy_expr(((InequProp*)p)->e1);
		_p->e2 = copy_expr(((InequProp*)p)->e2);
		_p->p = ((InequProp*)p)->p;
		return _p;
	}
	else{
		cout<<"error when copy prop."<<endl;
		exit(1);
	}
	return NULL;
}


void ARF::del_expr(Expr* e){
	//1.IntExpr, 2.SelectExpr, 3:VarExpr, 4:BinExpr, 5:StoreExpr
	if(typeid(*e) == typeid(IntExpr)){
		delete e;
		return;
	}
	else if(typeid(*e) == typeid(SelectExpr)){
		del_expr(((SelectExpr*)e)->a);
		del_expr(((SelectExpr*)e)->i);
		delete e;
		return;
	}
	else if(typeid(*e) == typeid(VarExpr)){
		delete e;
		return;
	}
	else if(typeid(*e) == typeid(BinExpr)){
		del_expr(((BinExpr*)e)->e1);
		del_expr(((BinExpr*)e)->e2);
		delete e;
		return;
	}
	else if(typeid(*e) == typeid(StoreExpr)){
		del_expr(((StoreExpr*)e)->a);
		del_expr(((StoreExpr*)e)->e);
		del_expr(((StoreExpr*)e)->i);
		delete e;
		return;
	}
	else {
		cout<<"error when delete expr."<<endl;
		exit(1);
	}
	return;
}

void ARF::del_prop(Prop* p){
	if(typeid(*p) == typeid(BoolProp)){
		delete p;
		return ;
	}
	else if(typeid(*p) == typeid(NegProp)){
		del_prop(((NegProp*)p)->p);
		delete p;
		return;
	}
	else if(typeid(*p) == typeid(BinProp)){
		del_prop(((BinProp*)p)->p1);
		del_prop(((BinProp*)p)->p2);
		delete p;
		return;
	}
	else if(typeid(*p) == typeid(InequProp)){
		del_expr(((InequProp*)p)->e1);
		del_expr(((InequProp*)p)->e2);
		delete p;
		return;
	}
	else{
		cout<<"error when delete prop."<<endl;
		exit(1);
	}
	return ;
}

void ARF::Remove_Descendant(ART_NODE* input){
	cout<<"Remove descendant."<<endl;
	stack<ART_NODE*> node_stack;
	Remove_from_Covermap(input);
	set<ART_NODE*>::iterator it = input->CHILD_list.begin();
	set<ART_NODE*>::iterator it_end = input->CHILD_list.end();
	while(it != it_end){
		node_stack.push(*it);
		cout<<"Push NODE "<<(*it)->get_node_id()<<" to delete stack."<<endl;
		it++;
	}
	input->CLEAR_CHILD();
	if(((UniNode*)input->cfa_node)->st == st_FUNC_Call){
		vector<summary_edge>::iterator it_se = summary_edge_set.begin();
		vector<summary_edge>::iterator it_se_end = summary_edge_set.end();
		while(it_se != it_se_end){
			vector<caller_tree>::iterator it_ct = caller_tree_table.begin();
			vector<caller_tree>::iterator it_ct_end = caller_tree_table.end();
			while(it_ct != it_ct_end){
				if(input == it_ct->caller){
					if(it_se->root == it_ct->root_of_tree){
						cout<<"remove summary edge: "<<it_se->function_name<<" ROOT:"<<it_se->root->get_node_id()<<" "<<Prop_to_String(it_se->p1)<<" -> "<<Prop_to_String(it_se->p2)<<endl;
						summary_edge_set.erase(it_se);
						func_to_root[((UniNode*)input->cfa_node)->name]->erase(it_ct->root_of_tree);
						cout<<"remove caller_tree_table: caller:"<<it_ct->caller->get_node_id()<<" root of tree:"<<it_ct->root_of_tree->get_node_id()<<" cphi:"<<Prop_to_String(it_ct->cphi)<<endl;
						caller_tree_table.erase(it_ct);

					}
				}
				it_ct++;
			}
			it_se++;
		}
		function_art_map[((UniNode*)input->cfa_node)->name]->erase(input);
	}
	else if(((UniNode*)input->cfa_node)->st == st_Return){
		//remove the summary edge
		vector<summary_edge>::iterator it_se = summary_edge_set.begin();
		vector<summary_edge>::iterator it_se_end = summary_edge_set.end();
		while(it_se != it_se_end){
			if(it_se->leaf == input){
				vector<ART_NODE*>::iterator it_artnode = it_se->call_node.begin();
				vector<ART_NODE*>::iterator it_artnode_end = it_se->call_node.end();
				while(it_artnode != it_artnode_end){//remove the node that use this summary edge
					cout<<"Push NODE "<<(*it_artnode)->get_node_id()<<" to delete stack(Return)"<<endl;
					node_stack.push(*it_artnode);
					(*it_artnode)->Parent->DELETE_CHILD(*it_artnode);
					it_artnode++;
				}
				cout<<"Delete summary edge:"<<it_se->function_name<<" root:"<<it_se->root->get_node_id()<<" leaf"<<it_se->leaf->get_node_id()<<" "<<Prop_to_String(it_se->p1)<<" -> "<<Prop_to_String(it_se->p2)<<endl;
				summary_edge_set.erase(it_se);
			}
		it_se++;
		}
	}

	set<ART_NODE*> delete_set;
	cout<<"initializing done."<<endl;
	while(!node_stack.empty()){
		ART_NODE* t = node_stack.top();
		node_stack.pop();
		cout<<"Removing NODE "<<t->get_node_id()<<endl;
		Remove_from_Covermap(t);
		Remove_from_processing_node(t);
		if(typeid(*(t->cfa_node)) == typeid(UniNode)){
			switch(((UniNode*)t->cfa_node)->st){
				case st_FUNC_Call:{
					cout<<"Delete function call: NODE "<<t->get_node_id()<<endl;
					cout<<"Function name:"<<((UniNode*)t->cfa_node)->name<<endl;
					set<ART_NODE*>::iterator it = t->CHILD_list.begin();
					set<ART_NODE*>::iterator it_end = t->CHILD_list.end();
					while(it != it_end){
						cout<<"Push NODE "<<(*it)->get_node_id()<<" to delete stack(the child of t)"<<endl;
						node_stack.push(*it);
						it++;
					}
					vector<caller_tree>::iterator it_ct = caller_tree_table.begin();
					vector<caller_tree>::iterator it_ct_end = caller_tree_table.end();
					while(it_ct != it_ct_end){//remove from caller tree table
						if(t == it_ct->caller){
							cout<<"remove caller_tree_table: caller:"<<it_ct->caller->get_node_id()<<" root of tree:"<<it_ct->root_of_tree->get_node_id()<<" cphi:"<<Prop_to_String(it_ct->cphi)<<endl;
							caller_tree_table.erase(it_ct);
						}
						it_ct++;
					}
					set<ART_NODE*>::iterator it_set_art = func_to_root[((UniNode*)t->cfa_node)->name]->begin();
					set<ART_NODE*>::iterator it_set_art_end = func_to_root[((UniNode*)t->cfa_node)->name]->end();
					while(it_set_art != it_set_art_end){//check which tree should be removed
						vector<caller_tree>::iterator it_ct = caller_tree_table.begin();
						vector<caller_tree>::iterator it_ct_end = caller_tree_table.end();
						bool remove = true;
						while(it_ct != it_ct_end){
							if(it_ct->root_of_tree == *it_set_art){
								cout<<"will not remove the tree: "<<(*it_set_art)->get_node_id()<<endl;
								remove = false;
							}
							it_ct++;
						}
						if(remove == true){
							node_stack.push(*it_set_art);
							cout<<"Push NODE "<<(*it_set_art)->get_node_id()<<" to delete stack(Func_Call)"<<endl;
							cout<<"remove NODE "<<(*it_set_art)->get_node_id()<<" from function to root map"<<endl;
							func_to_root[((UniNode*)t->cfa_node)->name]->erase(it_set_art);
						}
						it_set_art++;
					}
					cout<<"remove NODE "<<t->get_node_id()<<" from function art map"<<endl;
					function_art_map[((UniNode*)t->cfa_node)->name]->erase(t);
					cout<<"Delete NODE "<<t->get_node_id()<<endl;
					delete_set.insert(t);
					break;
				}
				case st_Return:{
					//remove the summary edge
					cout<<"Delete return node"<<endl;
					vector<summary_edge>::iterator it_se = summary_edge_set.begin();
					vector<summary_edge>::iterator it_se_end = summary_edge_set.end();
					while(it_se != it_se_end){
						if(it_se->leaf == t){
							vector<ART_NODE*>::iterator it_artnode = it_se->call_node.begin();
							vector<ART_NODE*>::iterator it_artnode_end = it_se->call_node.end();
							while(it_artnode != it_artnode_end){
								cout<<"Push NODE "<<(*it_artnode)->get_node_id()<<" to delete stack(Return)"<<endl;
								node_stack.push(*it_artnode);
								(*it_artnode)->Parent->DELETE_CHILD(*it_artnode);
								it_artnode++;
							}
							cout<<"Delete summary edge:"<<it_se->function_name<<" root:"<<it_se->root->get_node_id()<<" leaf"<<it_se->leaf->get_node_id()<<" "<<Prop_to_String(it_se->p1)<<" -> "<<Prop_to_String(it_se->p2)<<endl;
							summary_edge_set.erase(it_se);
						}
						it_se++;
					}
					cout<<"Delete NODE "<<t->get_node_id()<<endl;
					delete_set.insert(t);
					break;
				}
				default:{
					cout<<"Delete default node"<<endl;
					if(t->nCHILD() != 0){//if t has no child
						set<ART_NODE*>::iterator it = t->CHILD_list.begin();
						set<ART_NODE*>::iterator it_end = t->CHILD_list.end();
						while(it != it_end){
							cout<<"Push NODE "<<(*it)->get_node_id()<<" to delete stack(default)"<<endl;
							node_stack.push(*it);
							it++;
						}
						cout<<"Delete NODE "<<t->get_node_id()<<endl;
						delete_set.insert(t);
					}
				}
			}
		}
		else if(typeid(*(t->cfa_node)) == typeid(BinNode)){
			if(t->nCHILD() != 0){//if t has no child
				set<ART_NODE*>::iterator it = t->CHILD_list.begin();
				set<ART_NODE*>::iterator it_end = t->CHILD_list.end();
				while(it != it_end){
					cout<<"Push NODE "<<(*it)->get_node_id()<<" to delete stack(BinNode)"<<endl;
					node_stack.push(*it);
					it++;
				}
				cout<<"Delete NODE "<<t->get_node_id()<<endl;
				delete_set.insert(t);
			}
		}
		else if(typeid(*(t->cfa_node)) == typeid(BadNode)){
			cout<<"Delete Bad Node."<<endl;
		}
		else{
			cout<<"Error."<<endl;
		}
	}

	//delete the node in delete_set
	set<ART_NODE*>::iterator it_del = delete_set.begin();
	set<ART_NODE*>::iterator it_del_end = delete_set.begin();
	while(it_del != it_del_end){
		delete *it_del;
		delete_set.erase(it_del);
		it_del++;
	}
}

void ARF::Add_Tag_to_Expr(Expr* e, int func_l){
	//1.IntExpr, 2.SelectExpr, 3:VarExpr, 4:BinExpr, 5:StoreExpr
	if(typeid(*e) == typeid(IntExpr)){
		return;
	}
	else if(typeid(*e) == typeid(SelectExpr)){
		cout<<"Error: the function can't support SelectExpr."<<endl;
		exit(1);
		return;
	}
	else if(typeid(*e) == typeid(VarExpr)){
		vector<Expr*>::iterator gv_it = global_var->begin();
		vector<Expr*>::iterator gv_it_end = global_var->end();
		while(gv_it != gv_it_end){
			if(!strcmp(((VarExpr*)(*gv_it))->x, ((VarExpr*)e)->x)){//if it is global variable
				return;
			}
			gv_it++;
		}
		int len1 = strlen(((VarExpr*)e)->x);
		if((((VarExpr*)e)->x)[len1-1]>='0' && (((VarExpr*)e)->x)[len1-1]<='9'){
			for(int j=len1-2;j>=0;j--){
				if(!((((VarExpr*)e)->x)[j]>='0' && (((VarExpr*)e)->x)[j]<='9')){
					if((((VarExpr*)e)->x)[j]=='L' && (((VarExpr*)e)->x)[j-1]=='_'){//if there is a tag
						return;
					}
					else{//if there is no tag
						break;
					}
				}
			}
		}
		string s = (string("_L")+itoa(func_l));
		int len2 = s.length();
		for(int i=0 ; i<=len2 ; i++){
			(((VarExpr*)e)->x)[i+len1] = s[i];
		}
		return;
	}
	else if(typeid(*e) == typeid(BinExpr)){
		Add_Tag_to_Expr(((BinExpr*)e)->e1, func_l);
		Add_Tag_to_Expr(((BinExpr*)e)->e2, func_l);
		return;
	}
	else if(typeid(*e) == typeid(StoreExpr)){
		cout<<"Error: the function can't support StoreExpr."<<endl;
		exit(1);
		return;
	}
	else {
		cout<<"error when add tag to expr."<<endl;
		exit(1);
	}
	return;
}



void ARF::Add_Tag_to_All_Expr(Node* t,Prop* p, int func_l){//phi = phi[x/e]
	if(typeid(*p) == typeid(BoolProp)){
		return;
	}
	else if(typeid(*p) == typeid(NegProp)){
		Add_Tag_to_All_Expr(t, ((NegProp*)p)->p, func_l);
		return;
	}
	else if(typeid(*p) == typeid(BinProp)){
		Add_Tag_to_All_Expr(t, ((BinProp*)p)->p1, func_l);
		Add_Tag_to_All_Expr(t, ((BinProp*)p)->p2, func_l);
		return;
	}
	else if(typeid(*p) == typeid(InequProp)){
		if(typeid(*t) == typeid(UniNode)){
			if(((UniNode*)t)->st == st_FUNC_Call){
				if(CompareExpr(((UniNode*)t)->e1, ((InequProp*)p)->e1)){
					Add_Tag_to_Expr(((InequProp*)p)->e1, func_l);
				}
				else{
					Add_Tag_to_Expr(((InequProp*)p)->e1, func_l+1);
				}

				if(CompareExpr(((UniNode*)t)->e1, ((InequProp*)p)->e2)){
					Add_Tag_to_Expr(((InequProp*)p)->e2, func_l);
				}
				else{
					Add_Tag_to_Expr(((InequProp*)p)->e2, func_l+1);
				}
			}
			else{
				Add_Tag_to_Expr(((InequProp*)p)->e1, func_l);
				Add_Tag_to_Expr(((InequProp*)p)->e2, func_l);
			}
		}
		else{
			Add_Tag_to_Expr(((InequProp*)p)->e1, func_l);
			Add_Tag_to_Expr(((InequProp*)p)->e2, func_l);
		}
		return;
	}
	else{
		cout<<"error when add tag to all expr."<<endl;
		exit(1);
	}
	return;
}

void ARF::Remove_Tag_of_Expr(Expr* e){
	//1.IntExpr, 2.SelectExpr, 3:VarExpr, 4:BinExpr, 5:StoreExpr
	if(typeid(*e) == typeid(IntExpr)){
		return;
	}
	else if(typeid(*e) == typeid(SelectExpr)){
		cout<<"Error: this function can't support SelectExpr."<<endl;
		exit(1);
		return;
	}
	else if(typeid(*e) == typeid(VarExpr)){
		int len = strlen(((VarExpr*)e)->x);
		for(int i=len ; i==0 ; i--){
			if((((VarExpr*)e)->x)[i] == 'L'){
				if((((VarExpr*)e)->x)[i-1] == '_'){
					(((VarExpr*)e)->x)[i-1] = '\0';
					break;
				}
			}
		}
		return;
	}
	else if(typeid(*e) == typeid(BinExpr)){
		Remove_Tag_of_Expr(((BinExpr*)e)->e1);
		Remove_Tag_of_Expr(((BinExpr*)e)->e2);
		return;
	}
	else if(typeid(*e) == typeid(StoreExpr)){
		cout<<"Error: this function can't support StoreExpr."<<endl;
		exit(1);
		return;
	}
	else {
		cout<<"error when remove tag of expr."<<endl;
		exit(1);
	}
	return;
}

void ARF::Remove_Tag_of_All_Expr(Prop* p){
	if(typeid(*p) == typeid(BoolProp)){
		return;
	}
	else if(typeid(*p) == typeid(NegProp)){
		Remove_Tag_of_All_Expr(((NegProp*)p)->p);
		return;
	}
	else if(typeid(*p) == typeid(BinProp)){
		Remove_Tag_of_All_Expr(((BinProp*)p)->p1);
		Remove_Tag_of_All_Expr(((BinProp*)p)->p2);
		return;
	}
	else if(typeid(*p) == typeid(InequProp)){
		Remove_Tag_of_Expr(((InequProp*)p)->e1);
		Remove_Tag_of_Expr(((InequProp*)p)->e2);
		return;
	}
	else{
		cout<<"error when add tag to all expr."<<endl;
		exit(1);
	}
	return;
}

class backtrace_t{//the type for function Back_Trace
	public:
		ART_NODE* process_node;
		Prop* check_prop;
		vector<caller_tree>::iterator it;
		int function_level;
		backtrace_t(ART_NODE* p, Prop* c, vector<caller_tree>::iterator i, int l){
			//backtrace_t(process node, check prop, vector<caller_tree>::iterator);
			process_node = p;
			check_prop = c;
			it = i;
			function_level = l;
		}
};

void ARF::Back_Trace(ART_NODE* input){
	//Prop* ComputePre_Assign(Prop *phi, Expr *x, Expr *e);
	int function_level = 1;
	bool real_check = true;
	bool print = false;
	Prop* preprop = NULL;
	stack<Node*> trace_stack;
	Prop* check_prop = copy_prop(input->phi);
	ART_NODE* t_past = NULL;
	stack<backtrace_t> BackTraceStack;
	Add_Tag_to_All_Expr(input->Parent->cfa_node, check_prop, function_level);
	BackTraceStack.push(backtrace_t(input, check_prop, caller_tree_table.end(), function_level));

	while(!BackTraceStack.empty()){
		ART_NODE* t = BackTraceStack.top().process_node;
		Prop* check_prop = BackTraceStack.top().check_prop;
		vector<caller_tree>::iterator stack_it = BackTraceStack.top().it;
		int function_level = BackTraceStack.top().function_level;
		BackTraceStack.pop();
		if(print == false){
			trace_stack.push(t->cfa_node);
			if(typeid(*(t->cfa_node)) == typeid(UniNode)){
				cout<<"op:"<<((UniNode*)t->cfa_node)->statement<<endl;
			}
			else if(typeid(*(t->cfa_node)) == typeid(BinNode)){
				if(t_past->cfa_node == ((BinNode*)(t->cfa_node))->_true){
					cout<<"Guard = "<<Prop_to_String(((BinNode*)t->cfa_node)->p)<<endl;
				}
				else{
					cout<<"Guard = ~("<<Prop_to_String(((BinNode*)t->cfa_node)->p)<<")"<<endl;
				}
			}
			else{
				cout<<"Bad Node"<<endl;
			}

			t_past = t;
			cout<<"-------------------------------------------------------------------------------"<<endl;
			if(preprop == NULL)
				cout<<"preprop is NULL"<<endl;
			else
				cout<<"Preprop:"<<Prop_to_String(preprop)<<endl;
			cout<<"NODE "<<t->get_node_id()<<" cphi:"<<Prop_to_String(t->cphi)<<endl;
		}
		print = false;
		/////////////////////////////////////////////////////////////////
		cout<<"check prop: "<<Prop_to_String(check_prop)<<endl;

		if(interfaceSMT(check_prop)){//SAT is false, USAT is true
			real_check = false;
			//generate interpolant
			cout<<"------------------------------------Princess-----------------------------------"<<endl;
			vector<string> vs;
			piped_processt p(Dir_werePrincess, vs);
			Prop* interpolant = InterpolantInterface(t->cphi, preprop, p);
			if(interpolant==NULL){
				cout<<"interpolant is NULL"<<endl;
				exit(1);
			}
			cout<<"interpolant_o = "<<Prop_to_String(interpolant)<<endl;
			Remove_Tag_of_All_Expr(interpolant);
			cout<<"-------------------------------------------------------------------------------"<<endl;
			cout<<"Add an interpolant to NODE "<<t->get_node_id()<<endl;
			if(interpolant == NULL){
				cout<<"interpolant is NULL"<<endl;
				exit(1);
			}
			else{
				cout<<"Interpolant:"<<Prop_to_String(interpolant)<<endl;
			}
			//add predicate
			vector<Prop*>::iterator it_predicate = t->predicate.begin();
			vector<Prop*>::iterator it_predicate_end = t->predicate.end();
			while(it_predicate != it_predicate_end){//check whether the same predicate has been added to the node
				if(is_equal(*it_predicate, interpolant)){
					cout<<"add the same interpolant"<<Prop_to_String(interpolant)<<endl;
					//Graph_out("graph.dot");
					exit(1);
				}
				it_predicate++;
			}
			if(typeid(*(t->cfa_node)) == typeid(UniNode)){
				if((t->Parent == NULL) && (Func_Belong(t) != string("main"))){
					if(stack_it == caller_tree_table.end()){
						cout<<"caller tree table error."<<endl;
						exit(1);
					}
					if(((UniNode*)(stack_it->caller))->st == st_FUNC_Call){
						processing_node.push(stack_it->caller);
						caller_tree_table.erase(stack_it);
						continue;
					}
				}
			}
			t->predicate.push_back(interpolant);
			t->cfa_node->predicate.push_back(interpolant);
			Abstration(t);
			//remove all the descendant of the node
			Remove_Descendant(t);//need to be revised
			//do again
			processing_node.push(t);
			continue;
		}

		if(t->Parent == NULL){
			string func_name = Func_Belong(t);
			if(func_name == string("main")){
				cout<<"there is a real trace can lead to fault."<<endl;//it is real case
				//print the trace
				cout<<"Error Trace:"<<endl;
				Node* trace_past = NULL;
				while(!trace_stack.empty()){
					if(typeid(*(trace_stack.top())) == typeid(UniNode)){
						cout<<((UniNode*)trace_stack.top())->statement<<endl;
					}
					else if(typeid(*(trace_stack.top())) == typeid(BinNode)){
						if(trace_stack.top() == ((BinNode*)trace_past)->_true){
							cout<<"Branch(True):"<<Prop_to_String(((BinNode*)trace_stack.top())->p)<<endl;
						}
						else{
							cout<<"Branch(False):"<<Prop_to_String(((BinNode*)trace_stack.top())->p)<<endl;
						}
					}
					else{
						cout<<"Bad Node"<<endl;
					}
					trace_past = trace_stack.top();
					trace_stack.pop();
				}
				exit(1);

			}
			else{//to the function that calls it
				vector<caller_tree>::iterator it_ct = caller_tree_table.begin();
				vector<caller_tree>::iterator it_ct_end = caller_tree_table.end();
				while(it_ct != it_ct_end){
					if(it_ct->root_of_tree == t){//compute pre phi
						vector<Expr*>::iterator it_acp = ((UniNode*)it_ct->caller->cfa_node)->actualpara.begin();
						vector<Expr*>::iterator it_acp_end = ((UniNode*)it_ct->caller->cfa_node)->actualpara.end();
						vector<VarExpr*> formalpara = function_map[func_name]->GetFormPara();
						vector<VarExpr*>::iterator it_fp = formalpara.begin();
						vector<VarExpr*>::iterator it_fp_end = formalpara.end();
						preprop = check_prop;
						while(it_acp != it_acp_end){
							VarExpr* tempvar = new VarExpr;
							strcpy(tempvar->x, (string((*it_fp)->x)+"_"+func_name).c_str());
							Add_Tag_to_Expr(tempvar, function_level);
							//cout<<Expr2String(tempvar)<<" = "<<Expr2String(*it_acp)<<endl;
							//parameter assign
							Expr* ac_temp = copy_expr(*it_acp);
							Add_Tag_to_Expr(ac_temp, function_level);
							preprop = ComputePre_Assign(preprop, tempvar, ac_temp);
							it_acp++;
							it_fp++;
						}
						function_level--;
						Prop* append_prop = copy_prop(it_ct->caller->cphi);
						Add_Tag_to_All_Expr(it_ct->caller->Parent->cfa_node, append_prop, function_level);
						check_prop = Prop_Append(preprop, And, append_prop);
						t = it_ct->caller;
						BackTraceStack.push(backtrace_t(t, check_prop, caller_tree_table.end(), function_level));
						//print
						trace_stack.push(t->cfa_node);
						cout<<"op:"<<((UniNode*)t->cfa_node)->statement<<endl;
						t_past = t;
						cout<<"-------------------------------------------------------------------------------"<<endl;
						if(preprop == NULL)
							cout<<"preprop is NULL"<<endl;
						else
							cout<<"Preprop:"<<Prop_to_String(preprop)<<endl;
						cout<<"cphi:"<<Prop_to_String(t->cphi)<<endl;
					}
					it_ct++;
				}
				print = true;
				continue;
			}

		}
		if(typeid(*(t->Parent->cfa_node)) == typeid(UniNode)){
			//cout<<"Uni"<<endl;
			//cout<<"t->cfa_node:"<<t->get_node_id()<<endl;
			//cout<<"t->cphi:"<<Prop_to_String(t->cphi)<<endl;
			switch(((UniNode*)(t->Parent->cfa_node))->st){//type 1: assign, type 2: goto, type 3: return, type4: label, type5 funtion call
				case st_Assign:{//done
					//cout<<"assign"<<endl;
					//cout<<"((UniNode*)t->cfa_node)->statement = "<<((UniNode*)t->cfa_node)->statement<<endl;
					//cout<<"((UniNode*)t->Parent->cfa_node)->statement = "<<((UniNode*)t->Parent->cfa_node)->statement<<endl;
					Expr* cp_expr1 = copy_expr(((UniNode*)(t->Parent)->cfa_node)->e1);
					Expr* cp_expr2 = copy_expr(((UniNode*)(t->Parent)->cfa_node)->e2);
					Add_Tag_to_Expr(cp_expr1, function_level);
					Add_Tag_to_Expr(cp_expr2, function_level);
					preprop = ComputePre_Assign(check_prop, cp_expr1, cp_expr2);
					//cout<<"check_prop = "<<Prop_to_String(check_prop)<<endl;
					//cout<<"((UniNode*)(t->Parent)->cfa_node)->e1 = "<<Expr2String(((UniNode*)(t->Parent)->cfa_node)->e1)<<endl;
					//cout<<"((UniNode*)(t->Parent)->cfa_node)->e2 = "<<Expr2String(((UniNode*)(t->Parent)->cfa_node)->e2)<<endl;
					t = t->Parent;
					if((t->Parent == NULL) && (Func_Belong(t)!=string("main"))){
						vector<caller_tree>::iterator it_ct = caller_tree_table.begin();
						vector<caller_tree>::iterator it_ct_end = caller_tree_table.end();
						int cphi_i = 1;
						while(it_ct != it_ct_end){
							if(it_ct->root_of_tree == t){//compute pre phi
								cout<<"cphi "<<cphi_i<<": "<<Prop_to_String(it_ct->cphi)<<endl;
								Prop* append_prop = copy_prop(it_ct->cphi);
								Add_Tag_to_All_Expr(t->Parent->cfa_node, append_prop, function_level);
								check_prop = Prop_Append(preprop, And, append_prop);
								BackTraceStack.push(backtrace_t(t, check_prop, it_ct, function_level));
							}
							it_ct++;
						}
					}
					else{
						Prop* append_prop = copy_prop(t->cphi);
						if(t->Parent == NULL)
							Add_Tag_to_All_Expr(NULL, append_prop, function_level);
						else
							Add_Tag_to_All_Expr(t->Parent->cfa_node, append_prop, function_level);
						cout<<"app_prop="<<Prop_to_String(append_prop)<<endl;
						check_prop = Prop_Append(preprop, And, append_prop);
						BackTraceStack.push(backtrace_t(t, check_prop, caller_tree_table.end(), function_level));
					}
					}
					break;
				case st_Goto:{//done
					//cout<<"goto"<<endl;
					t = t->Parent;
					BackTraceStack.push(backtrace_t(t, check_prop, caller_tree_table.end(), function_level));
					}
					break;
				case st_Return:{//done
					//cout<<"return"<<endl;
					cout<<"st_Return will not occur in trace back function.(?!)"<<endl;
					}
					break;
				case st_Label:{//done
					//cout<<"label"<<endl;
					t = t->Parent;
					BackTraceStack.push(backtrace_t(t, check_prop, caller_tree_table.end(), function_level));
					}
					break;
				case st_FUNC_Call:{//done
					//cout<<"func"<<endl;
					//((UniNode*)call_to_return[t]->cfa_node)->e1 => get the return art node
					//cout<<Expr2String(((UniNode*)(t->Parent)->cfa_node)->e1)<<endl;
					//cout<<Expr2String(((UniNode*)call_to_return[t]->cfa_node)->e1)<<endl;
					Expr* copy_expr1 = ((UniNode*)(t->Parent)->cfa_node)->e1;
					Add_Tag_to_Expr(copy_expr1, function_level);
					Expr* copy_expr2 = ((UniNode*)call_to_return[t]->cfa_node)->e1;
					Add_Tag_to_Expr(copy_expr2, function_level+1);
					preprop = ComputePre_Assign(check_prop, copy_expr1, copy_expr2);
					t = call_to_return[t];
					function_level++;
					if((t->Parent == NULL) && (Func_Belong(t)!=string("main"))){
						vector<caller_tree>::iterator it_ct = caller_tree_table.begin();
						vector<caller_tree>::iterator it_ct_end = caller_tree_table.end();
						int cphi_i = 1;
						while(it_ct != it_ct_end){
							if(it_ct->root_of_tree == t){//compute pre phi
								Prop* append_prop = copy_prop(t->cphi);
								Add_Tag_to_All_Expr(t->Parent->cfa_node, append_prop, function_level);
								check_prop = Prop_Append(preprop, And, append_prop);
								BackTraceStack.push(backtrace_t(t, check_prop, it_ct, function_level));
							}
							it_ct++;
						}
					}
					else{
						Prop* append_prop = copy_prop(t->cphi);
						if(t->Parent == NULL)
							Add_Tag_to_All_Expr(NULL, append_prop, function_level);
						else
							Add_Tag_to_All_Expr(t->Parent->cfa_node, append_prop, function_level);

						check_prop = Prop_Append(preprop, And, append_prop);
						BackTraceStack.push(backtrace_t(t, check_prop, caller_tree_table.end(), function_level));
					}
					}
					break;
				default:
					;
			}
			//cout<<"preprop:"<<Prop_to_String(preprop)<<endl;
			//cout<<"check prop:"<<Prop_to_String(check_prop)<<endl;
		}
		else if(typeid(*(t->Parent->cfa_node)) == typeid(BinNode)){//done
			//cout<<"Bin"<<endl;
			//cout<<((BinNode*)t->cfa_node)->statement<<endl;
			//cout<<"t->cfa_node:"<<t->get_node_id()<<endl;
			//cout<<"t->cfa_node->_true:"<<((BinNode*)(t->cfa_node))->_true<<endl;
			//cout<<"t->cfa_node->_false:"<<((BinNode*)(t->cfa_node))->_false<<endl;
			if(t->cfa_node == ((BinNode*)(t->Parent->cfa_node))->_true){
				//cout<<"true"<<endl;
				preprop = check_prop;
				Prop* append_prop = copy_prop(((BinNode*)(t->Parent->cfa_node))->p);
				Add_Tag_to_All_Expr(t->Parent->Parent->cfa_node, append_prop, function_level);
				preprop = Prop_Append(preprop, And, append_prop);
			}
			else if(t->cfa_node == ((BinNode*)(t->Parent->cfa_node))->_false){
				//cout<<"false"<<endl;
				preprop = check_prop;
				Prop* append_prop = copy_prop(Neg_Prop(((BinNode*)(t->Parent->cfa_node))->p));
				Add_Tag_to_All_Expr(t->Parent->Parent->cfa_node, append_prop, function_level);
				preprop = Prop_Append(preprop, And, append_prop);
			}
			else{
				cout<<"error????????"<<endl;
			}
			//cout<<"preprop:"<<Prop_to_String(preprop)<<endl;
			//cout<<"t->Parent->cphi:"<<Prop_to_String(t->Parent->cphi)<<endl;
			t = t->Parent;
			if((t->Parent == NULL) && (Func_Belong(t)!=string("main"))){
				vector<caller_tree>::iterator it_ct = caller_tree_table.begin();
				vector<caller_tree>::iterator it_ct_end = caller_tree_table.end();
				while(it_ct != it_ct_end){
					if(it_ct->root_of_tree == t){//compute pre phi
						check_prop = Prop_Append(preprop, And, it_ct->cphi);
						BackTraceStack.push(backtrace_t(t, check_prop, it_ct, function_level));
					}
					it_ct++;
				}
			}
			else{
				Prop* append_prop = copy_prop(t->cphi);
				if(t->Parent == NULL)
					Add_Tag_to_All_Expr(NULL, append_prop, function_level);
				else
					Add_Tag_to_All_Expr(t->Parent->cfa_node, append_prop, function_level);
				check_prop = Prop_Append(preprop, And, append_prop);
				BackTraceStack.push(backtrace_t(t, check_prop, caller_tree_table.end(), function_level));

			}
		}
		else{
			cout<<"Error: TraceBack Error."<<endl;
			exit(1);
		}
		//check_prop = Prop_Append(preprop, And, t->Parent->cphi);
	}

	//ComputePre_Assign(t->phi, Expr *x, Expr *e);
	return;
}
/*
TermCheckT Term_Check(ART_NODE* t){
	if(t==NULL){
		return Term;
	}
	ART_NODE* temp = t;
	while((temp->Parent) != NULL){
		temp = temp->Parent;
	}
	if(&(func_to_root[string("main")]->find(temp))!=NULL){//if the node belongs to main
		if(typeid(*(t->cfa_node))==typeid(BadNode)){
			if(Trace_Back(t)){//is a real trace
				//cout the counterexample
				return Bad;//exit the program
			}
			else{//not a real trace
				return FakeTrace;
			}
		}
		else{
			return Others;
		}
	}
	else{//if the node belongs to other function
		//if(typeid(*(t->cfa_node))==typeid(TermNode)){
		//	t->set_traveled(true);
		//	return FunctionReturn;
		//}
		//else{
		//	return Others;
		//}
	}
	return Others;
}
*/
string ARF::Func_Belong(ART_NODE* t){
	t = get_initial(t);
	//cout<<"func belong: root is "<<t->get_node_id()<<endl;
	map<string, set<ART_NODE*>*>::iterator it_map = func_to_root.begin();
	map<string, set<ART_NODE*>*>::iterator it_map_end = func_to_root.end();
	while(it_map!=it_map_end){
		set<ART_NODE*>::iterator it = ((*it_map).second)->begin();
		set<ART_NODE*>::iterator it_end = ((*it_map).second)->end();
		//cout<<"it="<<(*it)<<endl;
		while(it!=it_end){
			if((*it)==t){
				return (*it_map).first;
			}
			++it;
		}
		++it_map;
	}
	return string("");
}

int new_index(){
	static int i;
	return i++;
}

string itoa(int in){//integer to ACII
	string temp_str("");
	if(in<0){
		temp_str+="-";
		abs(in);
	}
	do{
		char a = in%10+'0';
		in = in/10;
		temp_str += string(&a);
	}while(in);
	return temp_str;
}

void ARF::add_func_predicate(ART_NODE* t, vector<VarExpr*> formal_par, string func_name){

	vector<VarExpr*>::iterator it_f=formal_par.begin();
	vector<VarExpr*>::iterator it_f_end=formal_par.end();

	while(it_f!=it_f_end){//insert dummy
		Expr* temp_expr=new VarExpr;
		strcpy(((VarExpr*)temp_expr)->x, (string(((VarExpr*)(*it_f))->x)+"'"+func_name).c_str());
		Prop* prop_temp = new InequProp;
		((InequProp*)prop_temp)->e1=(*it_f);
		((InequProp*)prop_temp)->p=Eq;
		((InequProp*)prop_temp)->e2=temp_expr;
		(t->predicate).push_back(prop_temp);
		t->cphi = Prop_Append(t->cphi, And, prop_temp);
		//cout<<"cphi:"<<Prop_to_String(t->cphi)<<endl;
		it_f++;
	}
	return ;
}
Prop* ARF::ComputePost_Function(Prop* phi,vector<Expr*> actualpara, vector<VarExpr*> formal_par){
	vector<Expr*>::iterator it_a=actualpara.begin();
	vector<Expr*>::iterator it_a_end=actualpara.end();
	vector<VarExpr*>::iterator it_f=formal_par.begin();
	vector<VarExpr*>::iterator it_f_end=formal_par.end();
	Prop *phi_temp=NULL;
	while(it_a!=it_a_end){//parameter
		phi_temp = Prop_Append(ComputePost_Assign(phi, *it_f, *it_a), And, phi_temp);//append Prop
		it_f++;
		it_a++;
	}


	return phi_temp;
}

bool ARF::is_equal(ART_NODE* n1,ART_NODE* n2){
	if(n1->cfa_node != n2->cfa_node)
		return false;
	return interfaceSMT(Prop_Append(Neg_Prop(n1->phi), And, n2->phi)) && interfaceSMT(Prop_Append(Neg_Prop(n2->phi), And, n1->phi));
}


bool ARF::is_equal(Prop* p1, Prop* p2){
	return interfaceSMT(Prop_Append(Neg_Prop(p1), And, p2)) && interfaceSMT(Prop_Append(Neg_Prop(p2), And, p1));
}

ART_NODE* ARF::get_initial(ART_NODE* t){
	while(t->Parent != NULL){
		t = t->Parent;
	}
	return t;
}

void ARF::Print_Summary_edge(){
	//map<string, map<Prop*, Prop*> > summary_edge_map;
	vector<summary_edge>::iterator it = summary_edge_set.begin();
	vector<summary_edge>::iterator it_end = summary_edge_set.end();
	cout<<"-------------------------------------------------------------------------------"<<endl;
	cout<<"Summary_edge"<<endl;
	while(it != it_end){
		cout<<"Function:"<<it->function_name<<" ART:"<<it->root->get_node_id()<<" "<<Prop_to_String(it->p1)<<" -> "<<Prop_to_String(it->p2)<<endl;
		it++;
	}
	cout<<"-------------------------------------------------------------------------------"<<endl;
	return;
}

void ARF::add_cfa_predicate(ART_NODE* t){
	vector<Prop*>::iterator it = t->cfa_node->predicate.begin();
	vector<Prop*>::iterator it_end = t->cfa_node->predicate.end();
	while(it != it_end){
		bool add_flag = true;
		vector<Prop*>::iterator it2 = t->predicate.begin();
		vector<Prop*>::iterator it2_end = t->predicate.end();
		while(it2 != it2_end){
			if(is_equal(*it, *it2)){
				add_flag = false;
				break;
			}
			it2++;
		}
		if(add_flag == true)
			t->predicate.push_back(*it);
		it++;
	}
}

ARF::ARF(vector<CFA>* input, vector<Expr*>* gv){
	cout<<"-----------------------------------ARF Start-----------------------------------"<<endl;
	global_var = gv;
	//construct the root of main function and push it to the stack pr ocessing_node
	if(input->empty()){
		cout<<"the vector CFA is empty!"<<endl;
		return;
	}
	for(unsigned int i=0;i<input->size();i++){//construct function map
		function_map.insert(pair<string, CFA*>(string((*input)[i].GetId()), &(*input)[i]));
		cout<<"function "<<i<<" name:"<<(*input)[i].GetId()<<endl;
	}
	if(function_map[string("main")]==NULL){
		cout<<"Error: You have no main function in the program!"<<endl;
		exit(1);
	}
	Node* node_temp = function_map[string("main")]->GetInitNode();
	ART_NODE* artnode_temp = new ART_NODE(NULL, node_temp);//the first art node
	set<ART_NODE*>* ART_set=new set<ART_NODE*>;//call a function
	ART_set->insert(artnode_temp);
	func_to_root.insert(pair<string, set<ART_NODE*>*>(string("main"), ART_set));

	artnode_temp->cphi = new BoolProp;//set initial cphi
	((BoolProp*)(artnode_temp->cphi))->b = true;
	artnode_temp->phi = new BoolProp;//set initial phi
	((BoolProp*)(artnode_temp->phi))->b = true;
	Prop* Prop_temp = new BoolProp;//set predicate
	((BoolProp*)Prop_temp)->b = true;
	//cout<<"first Predicate:"<<Prop_to_String(Prop_temp)<<endl;
	artnode_temp->predicate.push_back(Prop_temp);//the first predicate is empty
	artnode_temp->cfa_node->predicate.push_back(Prop_temp);
	processing_node.push(artnode_temp);
	while(!processing_node.empty() ){//if processing stack is not empty
		ART_NODE* artnode_temp = processing_node.top();//pop the node that we are going to process
		Node* cfanode_temp = artnode_temp->cfa_node;
		cout<<"-------------------------------------------------------------------------------"<<endl;
		cout<<"processing NODE "<<artnode_temp->get_node_id()<<"......"<<endl;
		cout<<"cphi: "<<Prop_to_String(artnode_temp->cphi)<<endl;
		cout<<"phi: "<<Prop_to_String(artnode_temp->phi)<<endl;
		if(typeid(*cfanode_temp)==typeid(UniNode)){
			cout<<"op: "<<((UniNode*)cfanode_temp)->statement<<endl;
		}
		else if(typeid(*cfanode_temp)==typeid(BinNode)){
			cout<<"op: "<<Prop_to_String(((BinNode*)cfanode_temp)->p)<<" (BinNode)"<<endl;
		}
		else if(typeid(*cfanode_temp)==typeid(BadNode)){
			cout<<"Bad Node."<<endl;
		}
		else{
			cout<<"error."<<endl;
		}
		cout<<"Predicate:"<<endl;
		vector<Prop*>::iterator it_prop_vec = artnode_temp->predicate.begin();
		vector<Prop*>::iterator it_prop_vec_end = artnode_temp->predicate.end();
		while(it_prop_vec != it_prop_vec_end){
			cout<<"    "<<Prop_to_String(*it_prop_vec)<<endl;
			it_prop_vec++;
		}


		cout<<"-------------------------------------------------------------------------------"<<endl;
		processing_node.pop();
		//cout<<"st="<<((UniNode*)cfanode_temp)->st<<endl;
		if(is_Covered(artnode_temp)){//check cover
			artnode_temp->set_traveled(true);
			continue;
		}
		if(typeid(*cfanode_temp)==typeid(BadNode)){
			//back trace
			Print_Summary_edge();
			Back_Trace(artnode_temp);
			continue;

		}
		if(typeid(*cfanode_temp) == typeid(UniNode)){//command <=not yet~!
			/*if(((UniNode*)cfanode_temp)->next == NULL){
				artnode_temp->set_traveled(true);
				continue;//if it's the end
			}*/

			switch(((UniNode*)cfanode_temp)->st){//type 1: assign, type 2: goto, type 3: return, type4: label, type5 funtion call
				case st_Assign:{//x:=e => F[x/x'] /\ x:=e[x/x']
					//cout<<"st_Assign"<<endl;
					ART_NODE* t = new ART_NODE(artnode_temp, ((UniNode*)cfanode_temp)->next);//create a art node
					artnode_temp->ADD_CHILD(t);//set the ptr of the child
					t->predicate = artnode_temp->predicate;
					add_cfa_predicate(t);
					artnode_temp->set_traveled(true);//the parent is traveled
					t->cphi = ComputePost_Assign(artnode_temp->phi, ((UniNode*)cfanode_temp)->e1, ((UniNode*)cfanode_temp)->e2);
					//cout<<"Post_Assign:"<<Prop_to_String(t->cphi)<<endl;
					Abstration(t);
					//Prop_temp = Prop_Append(Neg_Prop(((UniNode*)cfanode_temp)->p), And, artnode_temp->phi);
					//for(int i = 0; i < (int)artnode_temp->predicate.size(); i++){
					//	cout<<"predicate: "<<Prop_to_String(t->predicate[i])<<endl;
					//}
					//cout<<"phi:"<<Prop_to_String(t->phi)<<endl;

					processing_node.push(t);
					}
					break;
				case st_FUNC_Call:{//x:=func(.....)
						//cout<<"st_FUNC_Call"<<endl;
						//cout<<"Prop:"<<Prop_to_String(artnode_temp->phi)<<endl;
						//cout<<"statement="<<((UniNode*)cfanode_temp)->statement<<endl;
						//cout<<"e1="<<Expr2String(((UniNode*)cfanode_temp)->e1)<<endl;
						//cout<<"e2="<<Expr2String(((UniNode*)cfanode_temp)->e2)<<endl;
                                                //cout<<"name=" << ((UniNode*)cfanode_temp)->name << endl;
						//ART_NODE* t = new ART_NODE(NULL, function_map[string(((UniNode*)cfanode_temp)->name)]->GetInitNode());
						ART_NODE* t = new ART_NODE(NULL, function_map[Expr2String(((UniNode*)cfanode_temp)->e2)]->GetInitNode());
						//t->predicate=add_func_predicate(artnode_temp);
						//vector<VarExpr*> FormPara = function_map[Expr2String(((UniNode*)cfanode_temp)->e2)]->GetFormPara();
						vector<VarExpr*> FormPara = function_map[Expr2String(((UniNode*)cfanode_temp)->e2)]->GetFormPara();
						if(FormPara.empty()){//formal parameter is empty
							cout<<"formal parameter is empty."<<endl;
							exit(1);
						}
						else{
							add_func_predicate(t, FormPara, Expr2String(((UniNode*)cfanode_temp)->e2));
						}
						add_cfa_predicate(t);
						t->cphi = Prop_Append(t->cphi, And, ComputePost_Function(artnode_temp->phi, ((UniNode*)(artnode_temp->cfa_node))->actualpara, function_map[Expr2String(((UniNode*)cfanode_temp)->e2)]->GetFormPara()));
						Abstration(t);
						if(is_Covered(Expr2String(((UniNode*)cfanode_temp)->e2), t, artnode_temp) == true){//function call is covered
							//use summary edge to compute post
							vector<summary_edge>::iterator it_se = summary_edge_set.begin();
							vector<summary_edge>::iterator it_se_end= summary_edge_set.end();
							while(it_se != it_se_end){
								if(is_equal(it_se->p1, t->phi)){//find the same phi1 of summary edge
									it_se->call_node.push_back(artnode_temp);
									//compute post
									ART_NODE* new_t = new ART_NODE(artnode_temp, ((UniNode*)cfanode_temp)->next);
									artnode_temp->ADD_CHILD(new_t);
									VarExpr* var_expr_temp = new VarExpr;
									strcpy(var_expr_temp->x, (string("var")+Int2String(new_index())+"'"+Func_Belong(it_se->root)).c_str());
									new_t->cphi = ComputePost_Assign(it_se->p2, ((UniNode*)cfanode_temp)->e1, var_expr_temp);
									new_t->predicate = artnode_temp->predicate;
									add_cfa_predicate(new_t);
									Abstration(new_t);
									processing_node.push(new_t);
									call_to_return.insert(pair<ART_NODE*, ART_NODE*>(new_t, it_se->leaf));
									it_se->call_node.push_back(new_t);
								}
								it_se++;
							}
							function_art_map[Expr2String(((UniNode*)cfanode_temp)->e2)]->insert(artnode_temp);

							continue;
						}
						else{//the function is not called before
							if(func_to_root.count(Expr2String(((UniNode*)cfanode_temp)->e2))==0){//create a new ART
								set<ART_NODE*>* temp_ART_set = new set<ART_NODE*>;
								temp_ART_set->insert(t);
								func_to_root.insert(pair<string, set<ART_NODE*>*>(Expr2String(((UniNode*)cfanode_temp)->e2), temp_ART_set));
							}
							else{
								func_to_root[Expr2String(((UniNode*)cfanode_temp)->e2)]->insert(t);
							}

							if(function_art_map.count(Expr2String(((UniNode*)cfanode_temp)->e2)) == 0){//add the function to art map
								set<ART_NODE*>* set_temp = new set<ART_NODE*>;
								set_temp->insert(artnode_temp);
								function_art_map.insert(pair<string, set<ART_NODE*>*>(Expr2String(((UniNode*)cfanode_temp)->e2), set_temp));
							}
							else{
								function_art_map[Expr2String(((UniNode*)cfanode_temp)->e2)]->insert(artnode_temp);
							}
							processing_node.push(t);
						}
					}
					break;
				case st_Label:{//L:S
					//cout<<"st_Label"<<endl;
					ART_NODE* t = new ART_NODE(artnode_temp, ((UniNode*)cfanode_temp)->next);//create a art node
					artnode_temp->ADD_CHILD(t);//set the ptr of the child
					t->predicate = artnode_temp->predicate;
					add_cfa_predicate(t);
					artnode_temp->set_traveled(true);
					t->phi = artnode_temp->phi;
					t->cphi = artnode_temp->cphi;
					processing_node.push(t);
					}
					break;
				case st_Goto:{//goto or continue or break or return
					//cout<<"st_Goto"<<endl;
					ART_NODE* t = new ART_NODE(artnode_temp, ((UniNode*)cfanode_temp)->next);//create a art node

					artnode_temp->ADD_CHILD(t);//set the ptr of the child
					t->predicate = artnode_temp->predicate;
					add_cfa_predicate(t);
					artnode_temp->set_traveled(true);//the parent is traveled
					t->phi = artnode_temp->phi;
					t->cphi = artnode_temp->cphi;
					processing_node.push(t);
				}
					break;
				case st_Return:{//to be continue
					//cout<<"st_Return"<<endl;
					//vector<Prop*> Summary_Edge
					//map<string, Summary_Edge> sum_edge_map
					string func_name = Func_Belong(artnode_temp);
					//cout<<"Func_Belong:"<<Func_Belong(artnode_temp)<<endl;
					if(function_art_map.count(func_name) == 0){//no node call this function
						if(((UniNode*)cfanode_temp)->next == NULL)
							cout<<"No one call this function. Function Name:"<<func_name<<endl;
					}
					else{//add new summary edge
						summary_edge s;
						s.function_name = func_name;
						s.root = get_initial(artnode_temp);
						s.leaf = artnode_temp;
						s.p1 = s.root->phi;
						s.p2 = artnode_temp->phi;

						cout<<"add summary edge:["<<func_name<<"]"<<Prop_to_String(s.root->phi)<<" -> "<<Prop_to_String(artnode_temp->phi)<<endl;

						//compute post using summary edge
						set<ART_NODE*>::iterator it_artnode_set = function_art_map[func_name]->begin();
						set<ART_NODE*>::iterator it_artnode_set_end = function_art_map[func_name]->end();
						while(it_artnode_set != it_artnode_set_end){
							ART_NODE* eq_t = new ART_NODE(NULL, function_map[func_name]->GetInitNode());
							add_func_predicate(eq_t, function_map[func_name]->GetFormPara(), func_name);
							add_cfa_predicate(eq_t);
							eq_t->cphi = Prop_Append(eq_t->cphi, And, ComputePost_Function((*it_artnode_set)->phi, ((UniNode*)((*it_artnode_set)->cfa_node))->actualpara, function_map[func_name]->GetFormPara()));
							Abstration(eq_t);

							if(is_equal(eq_t, s.root)){//use summary edge to compute post
								if(((UniNode*)((*it_artnode_set)->cfa_node))->e1 != NULL){
									cout<<"add summary edge to compute post @NODE "<<(*it_artnode_set)->get_node_id()<<"."<<endl;
									ART_NODE* new_t = new ART_NODE(*it_artnode_set, ((UniNode*)((*it_artnode_set)->cfa_node))->next);
									(*it_artnode_set)->ADD_CHILD(new_t);
									VarExpr* var_expr_temp = new VarExpr;
									strcpy(var_expr_temp->x, (string("var")+Int2String(new_index())+"'"+func_name).c_str());
									new_t->cphi = ComputePost_Assign(s.leaf->phi, ((UniNode*)((*it_artnode_set)->cfa_node))->e1, ((UniNode*)s.leaf->cfa_node)->e1);

									new_t->predicate = (*it_artnode_set)->predicate;
									add_cfa_predicate(new_t);
									Abstration(new_t);
									processing_node.push(new_t);
									call_to_return.insert(pair<ART_NODE*, ART_NODE*>(new_t, s.leaf));
									s.call_node.push_back(new_t);
								}
								else{

								}
							}
							it_artnode_set++;
						}
						summary_edge_set.push_back(s);

					}
					/*
					ART_NODE* art_root = get_initial(artnode_temp);
					map<ART_NODE*, ART_NODE*>::iterator it_temp = call_to_callee.begin();
					map<ART_NODE*, ART_NODE*>::iterator it_temp_end = call_to_callee.end();
					while(it_temp != it_temp_end){
						if(it_temp->second == art_root){
							ART_NODE* t = new ART_NODE(it_temp->first, ((UniNode*)it_temp->first->cfa_node)->next);
							it_temp->first->ADD_CHILD(t);

							//cout<<"it_temp->first="<<it_temp->first<<endl;
							//cout<<"cfa="<<((UniNode*)it_temp->first->cfa_node)->next<<endl;
							VarExpr* var_expr_temp = new VarExpr;
							strcpy(var_expr_temp->x, (string("var")+Int2String(new_index())+"'"+Func_Belong(art_root)).c_str());
							t->cphi = ComputePost_Assign(artnode_temp->phi, ((UniNode*)it_temp->first->cfa_node)->e1, var_expr_temp);
							t->predicate = it_temp->first->predicate;
							Abstration(t);
							processing_node.push(t);
							//call_to_return.insert(pair<ART_NODE*, ART_NODE*>(t, artnode_temp));
							break;
						}
						else{
							cout<<"not found"<<endl;
						}
						it_temp++;
					}
					*/
					break;
				}
				default:
					;
			}
		}
		else{//if(guard){....}else{....} or while(guard){....} or assert(guard)
			if(typeid(*cfanode_temp)==typeid(BinNode)){//while b do  s | if b then s else s
				//cout<<"BinNode!!"<<endl;
				//cout<<"predicate size:"<<(int)artnode_temp->predicate.size()<<endl;
				//for(int i = 0; i < (int)artnode_temp->predicate.size(); i++){
				//	cout<<"predicate: "<<Prop_to_String(artnode_temp->predicate[i])<<endl;
				//}
				//cout<<"(BinNode)phi: "<<Prop_to_String(artnode_temp->phi)<<endl;
				Prop* guard_temp = Prop_Append(((BinNode*)cfanode_temp)->p, And, artnode_temp->phi);
				if(!interfaceSMT(guard_temp)){//if guard is true
					//cout<<"guard_temp="<<Prop_to_String(guard_temp)<<"(guard is true)"<<endl;
					ART_NODE* t = new ART_NODE(artnode_temp, ((BinNode*)cfanode_temp)->_true);//create a art node
					artnode_temp->ADD_CHILD(t);//set the ptr of the child
					t->predicate = artnode_temp->predicate;
					add_cfa_predicate(t);
					t->cphi = guard_temp;
					Abstration(t);
					processing_node.push(t);
				}
				else {
					delete guard_temp;
				}
				guard_temp = Prop_Append(Neg_Prop(((BinNode*)cfanode_temp)->p), And, artnode_temp->phi);

				if(!interfaceSMT(guard_temp)){//if guard is false
					//cout<<"guard_temp="<<Prop_to_String(guard_temp)<<"(guard is false)"<<endl;
					ART_NODE* t = new ART_NODE(artnode_temp, ((BinNode*)cfanode_temp)->_false);//create a art node
					artnode_temp->ADD_CHILD(t);//set the ptr of the child

					t->predicate = artnode_temp->predicate;
					add_cfa_predicate(t);
					t->cphi = guard_temp;
					Abstration(t);
					processing_node.push(t);

				}
				else{//the guard_temp is no use
					delete guard_temp;
				}
				artnode_temp->set_traveled(true);
			}
			else{//if it is not a BinNode or UniNode
				cout<<cfanode_temp<<"=>error at Node"<<artnode_temp->get_node_id()<<". the node is neither a UniNode or a BinNode."<<endl;
				exit(1);
			}
		}
		//creat the edge from the exist ART node to new ART node
	}
}


void ARF::Print_ART(ART_NODE* t){
	if(t->nCHILD() == 0){//print itself
		return ;
	}
	else{
		//cout<<"\"node "<<t->get_node_id()<<"\" -> \""<<Prop_to_String(t->phi)<<"\";"<<endl;
		set<ART_NODE*>::iterator it = t->CHILD_list.begin();
		set<ART_NODE*>::iterator it_end = t->CHILD_list.end();
		while(it != it_end){
			if(typeid(*(t->cfa_node)) == typeid(UniNode)){
				if(typeid(*(*it)->cfa_node) == typeid(BadNode))
					cout<<"\"N"<<t->get_node_id()<<"("<<Prop_to_String(t->phi)<<")\" -> \"BAD("<<Prop_to_String((*it)->phi)<<")\""<<"[label = \""<<((UniNode*)(t->cfa_node))->statement<<"\"]"<<";"<<endl;
				//else if(typeid(*(*it)->cfa_node) == typeid(TermNode))
					//cout<<"\"N"<<t->get_node_id()<<"("<<Prop_to_String(t->phi)<<")\" -> \"TERM("<<Prop_to_String((*it)->phi)<<")\""<<"[label = \""<<((UniNode*)(t->cfa_node))->statement<<"\"]"<<";"<<endl;
				else
					cout<<"\"N"<<t->get_node_id()<<"("<<Prop_to_String(t->phi)<<")\" -> \"N"<<(*it)->get_node_id()<<"("<<Prop_to_String((*it)->phi)<<")\""<<"[label = \""<<((UniNode*)(t->cfa_node))->statement<<"\"]"<<";"<<endl;
			}
			else if(typeid(*(t->cfa_node)) == typeid(BinNode)){
				if(typeid(*(*it)->cfa_node) == typeid(BadNode))
					cout<<"\"N"<<t->get_node_id()<<"("<<Prop_to_String(t->phi)<<")\" -> \"BAD("<<Prop_to_String((*it)->phi)<<")\""<<"[label = \""<<Prop_to_String((*it)->phi)<<"\"]"<<";"<<endl;
				//else if(typeid(*(*it)->cfa_node) == typeid(TermNode))
					//cout<<"\"N"<<t->get_node_id()<<"("<<Prop_to_String(t->phi)<<")\" -> \"TERM("<<Prop_to_String((*it)->phi)<<")\""<<"[label = \""<<Prop_to_String((*it)->phi)<<"\"]"<<";"<<endl;
				else
					cout<<"\"N"<<t->get_node_id()<<"("<<Prop_to_String(t->phi)<<")\" -> \"N"<<(*it)->get_node_id()<<"("<<Prop_to_String((*it)->phi)<<")\""<<"[label = \""<<Prop_to_String((*it)->phi)<<"\"]"<<";"<<endl;
			}

			Print_ART(*it);
			++it;
		}

	}
}

void ARF::Print_ARFile(ART_NODE* t, ofstream& outfile){
	if(t->nCHILD() == 0){//print itself
		return ;
	}
	else{
		//cout<<"\"node "<<t->get_node_id()<<"\" -> \""<<Prop_to_String(t->phi)<<"\";"<<endl;
		set<ART_NODE*>::iterator it = t->CHILD_list.begin();
		set<ART_NODE*>::iterator it_end = t->CHILD_list.end();
		while(it != it_end){
			//cout<<"NODE "<<(*it)->get_node_id()<<" graph out."<<endl;
			cout<<"NODE "<<(*it)->get_node_id()<<endl;
			cout<<"cphi: "<<Prop_to_String((*it)->cphi)<<endl;
			cout<<"phi: "<<Prop_to_String((*it)->phi)<<endl;
			if(typeid(*(*it)->cfa_node)==typeid(UniNode)){
				cout<<"op: "<<((UniNode*)(*it)->cfa_node)->statement<<endl;
			}
			else if(typeid(*(*it)->cfa_node)==typeid(BinNode)){
				cout<<"op: "<<Prop_to_String(((BinNode*)(*it)->cfa_node)->p)<<" (BinNode)"<<endl;
			}
			else if(typeid(*(*it)->cfa_node)==typeid(BadNode)){
				cout<<"Bad Node."<<endl;
			}
			else{
				cout<<"error."<<endl;
			}
			cout<<"Predicate:"<<endl;
			vector<Prop*>::iterator it_prop_vec = (*it)->predicate.begin();
			vector<Prop*>::iterator it_prop_vec_end = (*it)->predicate.end();
			while(it_prop_vec != it_prop_vec_end){
				cout<<"    "<<Prop_to_String(*it_prop_vec)<<endl;
				it_prop_vec++;
			}
			cout<<"-------------------------------------------------------------------------------"<<endl;
			if(typeid(*(t->cfa_node)) == typeid(UniNode)){
				if(typeid(*(*it)->cfa_node) == typeid(BadNode))
					outfile<<"\"N"<<t->get_node_id()<<"< "<<Prop_to_String(t->phi)<<" >\" -> \"BAD< "<<Prop_to_String((*it)->phi)<<" >\""<<"[label = \""<<((UniNode*)(t->cfa_node))->statement<<"\"]"<<";"<<endl;
				else
					outfile<<"\"N"<<t->get_node_id()<<"< "<<Prop_to_String(t->phi)<<" >\" -> \"N"<<(*it)->get_node_id()<<"< "<<Prop_to_String((*it)->phi)<<" >\""<<"[label = \""<<((UniNode*)(t->cfa_node))->statement<<"\"]"<<";"<<endl;
			}
			else if(typeid(*(t->cfa_node)) == typeid(BinNode)){
				if(typeid(*(*it)->cfa_node) == typeid(BadNode))
					outfile<<"\"N"<<t->get_node_id()<<"< "<<Prop_to_String(t->phi)<<" >\" -> \"BAD< "<<Prop_to_String((*it)->phi)<<" >\""<<"[label = \""<<Prop_to_String((*it)->phi)<<"\"]"<<";"<<endl;
				else{
					if(((BinNode*)t->cfa_node)->_true){
						outfile<<"\"N"<<t->get_node_id()<<"< "<<Prop_to_String(t->phi)<<" >\" -> \"N"<<(*it)->get_node_id()<<"< "<<Prop_to_String((*it)->phi)<<" >\""<<"[label = \""<<Prop_to_String(((BinNode*)t->cfa_node)->p)<<"\"]"<<";"<<endl;
					}
					else{
						outfile<<"\"N"<<t->get_node_id()<<"< "<<Prop_to_String(t->phi)<<" >\" -> \"N"<<(*it)->get_node_id()<<"< "<<Prop_to_String((*it)->phi)<<" >\""<<"[label = \"~"<<Prop_to_String(((BinNode*)t->cfa_node)->p)<<"\"]"<<";"<<endl;
					}
				}
			}
			Print_ARFile(*it, outfile);
			++it;
		}

	}
}

void ARF::Graph_out(char* c){
	ofstream outfile(c);
	if(!outfile){
		cerr <<"error: unable to open output file:"<<outfile<<endl;
		exit(1);
	}

	outfile<<"digraph G {"<<endl;
	map<string, set<ART_NODE*>*>::iterator func_it = func_to_root.begin();
	map<string, set<ART_NODE*>*>::iterator func_it_end = func_to_root.end();
	while(func_it != func_it_end){
		set<ART_NODE*>::iterator set_root_it = func_it->second->begin();
		set<ART_NODE*>::iterator set_root_it_end = func_it->second->end();
		while(set_root_it != set_root_it_end){
			Print_ARFile(*set_root_it, outfile);
			++set_root_it;
		}
		++func_it;
	}
	outfile<<"}"<<endl;
	return ;
}

void ARF::Graph_out(){
	cout<<"digraph G {"<<endl;
	map<string, set<ART_NODE*>*>::iterator func_it = func_to_root.begin();
	map<string, set<ART_NODE*>*>::iterator func_it_end = func_to_root.end();
	while(func_it != func_it_end){
		set<ART_NODE*>::iterator set_root_it = func_it->second->begin();
		set<ART_NODE*>::iterator set_root_it_end = func_it->second->end();
		while(set_root_it != set_root_it_end){
			Print_ART(*set_root_it);
			++set_root_it;
		}
		++func_it;
	}
	cout<<"}"<<endl;
	return ;
}

/*
 * UniNode:
 * x = e | skip | x = id(e1, e2, ...) | return x | L: s | goto L | break | continue
 *
 * BinNode:
 * while b do  s | if b then s else s
 */

/*
 * trace back function
 * if the trace is a real trace it will print the counterexample then return true
 * else it will add the interpolant to ART node then push this node to processing stack return false
 */


/**************************************
 * the function Abstration
 **************************************/

void Abstration(ART_NODE* t){
	for(int i = 0; i < (int)t->predicate.size(); i++){//abstract post
		Prop* prop_temp1 = Prop_Append(Neg_Prop(t->predicate[i]), And, t->cphi);
		Prop* prop_temp2 = Prop_Append(t->predicate[i], And, t->cphi);
		if(interfaceSMT(prop_temp1)){
			if(t->phi == NULL){
				t->phi = t->predicate[i];
			}
			else{
				t->phi = Prop_Append(t->predicate[i], And, t->phi);
			}
		}
		else if(interfaceSMT(prop_temp2)){
			if(t->phi == NULL){
				t->phi = Neg_Prop(t->predicate[i]);
			}
			else{
				t->phi = Prop_Append(Neg_Prop(t->predicate[i]), And, t->phi);
			}
		}
		else{
			if(t->phi == NULL){
				t->phi = new BoolProp;
				((BoolProp*)t->phi)->b = true;
			}
			else{
				Prop* true_temp = new BoolProp;
				((BoolProp*)true_temp)->b = true;
				t->phi = Prop_Append(true_temp, And, t->phi);
			}
		}
	}
}

/**************************************
 * the functions for Prop
 **************************************/

Prop* Prop_Append(Prop *p1, LogicType l, Prop *p2){
	if(p1==NULL)return p2;
	if(p2==NULL)return p1;
    Prop *phi = new BinProp(p1, l, p2);
    /*((BinProp*)phi)->p1 = p1;
    ((BinProp*)phi)->p2 = p2;
    ((BinProp*)phi)->l = l;*/
    return phi;
}

Prop* Neg_Prop(Prop *p){
    Prop *phi = new NegProp;
    ((NegProp*)phi)->p = p;
    return phi;
}


/**************************************
 * the functions for ComputePost_Assign
 **************************************/

Expr *ReplaceExpr(Expr *e, Expr *x){
    //CFA cfa;
    Expr *e_1;
    e_1 = NULL;
    string s;
    if(typeid(*e) == typeid(VarExpr)){
        if(CompareExpr(e, x)){
            e_1 = new VarExpr;
            strcpy(((VarExpr*)e_1)->x, (string(((VarExpr*)e)->x)+"_" ).c_str());//+ Int2String(new_index())).c_str());
        }
        else{
            e_1 = e;
        }
        //cout << "Var " << ((VarExpr*)e_1)->s << endl;
    }
    else if(typeid(*e) == typeid(IntExpr)){
        e_1 = new IntExpr;
        ((IntExpr*)e_1)->i = ((IntExpr*)e)->i;
        //cout << "Int " << ((IntExpr*)e)->i << endl;
    }
    else /*if(typeid(*e) == typeid(ArrayExpr)){
        //cout << "Array" << endl;
        if(CompareExpr(e, x)){
            e_1 = new ArrayExpr;
            s = string(((ArrayExpr*)e)->n);
            cout<<"ReplaceExpr_i="<<ReplaceExpr_i<<endl;
            s = s+ "\'" + Int2String(ReplaceExpr_i);
            strcpy(((ArrayExpr*)e)->n, s.c_str());
            ReplaceExpr_i++;
        }
        else{
            e_1 = e;
        }
    }
    else */if(typeid(*e) == typeid(BinExpr)){
        //cout << "Bin" << endl;
        e_1 = new BinExpr;
        ((BinExpr*)e_1)->e1 = ReplaceExpr(((BinExpr*)e)->e1, x);
        ((BinExpr*)e_1)->e2 = ReplaceExpr(((BinExpr*)e)->e2, x);
        ((BinExpr*)e_1)->op = ((BinExpr*)e)->op;
    }
    //cfa.PrintExpr(e_1); cout << endl;
    return e_1;
}

Prop* ReplaceProp(Prop* phi, Expr* e){
    //CFA cfa;
    Prop *phi_1;
    phi_1 = NULL;
    if(typeid(*phi) == typeid(BoolProp)){
        phi_1 = new BoolProp;
        ((BoolProp*)phi_1)->b = ((BoolProp*)phi)->b;
    }
    else if(typeid(*phi) == typeid(NegProp)){
        phi_1 = new NegProp;
        ((NegProp*)phi_1)->p = ReplaceProp(((NegProp*)phi)->p, e);
    }
    else if(typeid(*phi) == typeid(BinProp)){
        phi_1 = new BinProp;
        ((BinProp*)phi_1)->p1 = ReplaceProp(((BinProp*)phi)->p1, e);
        ((BinProp*)phi_1)->p2 = ReplaceProp(((BinProp*)phi)->p2, e);
        ((BinProp*)phi_1)->l = ((BinProp*)phi)->l;
    }
    else if(typeid(*phi) == typeid(InequProp)){
        phi_1 = new InequProp;
        if(CompareExpr(((InequProp*)phi)->e1, e)){
            ((InequProp*)phi_1)->e1 = ReplaceExpr(((InequProp*)phi)->e1, e);
        }
        else{
            ((InequProp*)phi_1)->e1 = ((InequProp*)phi)->e1;
        }
        if(CompareExpr(((InequProp*)phi)->e2, e)){
            ((InequProp*)phi_1)->e2 = ReplaceExpr(((InequProp*)phi)->e2, e);
        }
        else{
            ((InequProp*)phi_1)->e2 = ((InequProp*)phi)->e2;
        }
        ((InequProp*)phi_1)->p = ((InequProp*)phi)->p;
        //cfa.PrintProp(phi_1); cout << endl;
    }
    else{
    }
    return phi_1;
}

bool FindX(Prop *phi, Expr *x){
    //CFA cfa;
    bool result;
    result = true;
    if(typeid(*phi) == typeid(BoolProp)){ result = false; }
    else if(typeid(*phi) == typeid(NegProp)){
        result = FindX(((NegProp*)phi)->p, x);
    }
    else if(typeid(*phi) == typeid(BinProp)){
        result = FindX(((BinProp*)phi)->p1, x) | FindX(((BinProp*)phi)->p2, x);
    }
    else if(typeid(*phi) == typeid(InequProp)){
        if(CompareExpr(((InequProp*)phi)->e1, x) || CompareExpr(((InequProp*)phi)->e2, x)){
            return true;
        }
        else{ return false; }
    }
    else{
    }
    return result;
}

bool FindX1(Expr *e, Expr *x){
    if(typeid(*e) == typeid(*x)){
        if(typeid(*e) == typeid(IntExpr)){
            if(((IntExpr*)e)->i == ((IntExpr*)x)->i){ return true; }
            else{ return false; }
        }
        else /*if(typeid(*e) == typeid(ArrayExpr)){
            if(strcmp(((ArrayExpr*)e)->n, ((ArrayExpr*)x)->n) == 0 && FindX1(((ArrayExpr*)e)->e, ((ArrayExpr*)x)->e)){ return true; }
            else{ return false; }
        }
        else */if(typeid(*e) == typeid(VarExpr)){
            if(strcmp(((VarExpr*)e)->x, ((VarExpr*)x)->x) == 0){ return true; }
            else{ return false; }
        }
        else if(typeid(*e) == typeid(BinExpr)){
            if(FindX1(((BinExpr*)e)->e1, ((BinExpr*)x)->e1) && FindX1(((BinExpr*)e)->e1, ((BinExpr*)x)->e1)){ return true; }
            else{ return false; }
        }
        else{
        }
    }
    else{
        if(typeid(*e) == typeid(IntExpr)){ return false; }
        //else if(typeid(*e) == typeid(ArrayExpr)){ return false; }
        else if(typeid(*e) == typeid(VarExpr)){ return false; }
        else if(typeid(*e) == typeid(BinExpr)){
            if(FindX1(((BinExpr*)e)->e1, x) || FindX1(((BinExpr*)e)->e2, x)){ return true; }
            else{ return false; }
        }
    }
    return false;
}

Prop* ARF::ComputePost_Assign(Prop *phi, Expr *x, Expr *e){//compute post phi for assign
    //CFA cfa;
    //cout << "test XXXX = " << StringProp(phi) << endl;
    Prop *phi_1, *x_1;
    phi_1 = new BinProp;
    x_1 = new InequProp;
    if(FindX(phi, x) == true){
        ((BinProp*)phi_1)->p1 = ReplaceProp(phi, x);
        ((BinProp*)phi_1)->l = And;

        ((InequProp*)x_1)->e1 = x;
        ((InequProp*)x_1)->e2 = ReplaceExpr(e, x);
        ((InequProp*)x_1)->p = Eq;
        ((BinProp*)phi_1)->p2 = x_1;
    }
    else{
        ((BinProp*)phi_1)->p1 = phi;
        ((BinProp*)phi_1)->l = And;
        ((InequProp*)x_1)->e1 = x;
        if(FindX1(e, x)){
        	((InequProp*)x_1)->e2 = ReplaceExpr(e, x);
        }
        else{
        	((InequProp*)x_1)->e2 = e;
        }
        ((InequProp*)x_1)->p = Eq;
        ((BinProp*)phi_1)->p2 = x_1;
    }
    //cfa.PrintProp(x_1); cout << endl;
    //cfa.PrintProp(((BinProp*)phi_1)->p1); cout << endl;
    //cfa.PrintProp(phi_1); cout << endl;
    return phi_1;
}

Prop* ReplacePropPre(Prop* phi, Expr* x, Expr* e){
    //CFA cfa;
    Prop *phi_1 = NULL;
    if(typeid(*phi) == typeid(BoolProp)){
        phi_1 = new BoolProp;
        ((BoolProp*)phi_1)->b = ((BoolProp*)phi)->b;
    }
    else if(typeid(*phi) == typeid(NegProp)){
        phi_1 = new NegProp;
        ((NegProp*)phi_1)->p = ReplacePropPre(((NegProp*)phi)->p, x, e);
    }
    else if(typeid(*phi) == typeid(BinProp)){
        phi_1 = new BinProp;
        ((BinProp*)phi_1)->p1 = ReplacePropPre(((BinProp*)phi)->p1, x, e);
        ((BinProp*)phi_1)->p2 = ReplacePropPre(((BinProp*)phi)->p2, x, e);
        ((BinProp*)phi_1)->l = ((BinProp*)phi)->l;
    }
    else if(typeid(*phi) == typeid(InequProp)){
        phi_1 = new InequProp;
        if(CompareExpr(((InequProp*)phi)->e1, x)){
            ((InequProp*)phi_1)->e1 = e;
        }
        else{
            ((InequProp*)phi_1)->e1 = ((InequProp*)phi)->e1;
        }
        if(CompareExpr(((InequProp*)phi)->e2, x)){
            ((InequProp*)phi_1)->e2 = e;
        }
        else{
            ((InequProp*)phi_1)->e2 = ((InequProp*)phi)->e2;
        }
        ((InequProp*)phi_1)->p = ((InequProp*)phi)->p;
        //cfa.PrintProp(phi_1); cout << endl;
    }
    else{
    }
    return phi_1;
}

Prop* ARF::ComputePre_Assign(Prop *phi, Expr *x, Expr *e){//compute pre phi for assign
    //Prop *phi_1, *x_1;
    //phi_1 = new BinProp;
    //x_1 = new InequProp;
    if(FindX(phi, x) == true){
    	//cout<<"Found it!"<<endl;
    	//cout<<"phi = "<<Prop_to_String(phi)<<endl;
        Prop* phi_1 = ReplacePropPre(phi, x, e);
        //cout<<"phi' = "<<Prop_to_String(phi_1)<<endl;
        return phi_1;
    }
    else{
    	return phi;
    }


}
/*
 * for debug
 */
string StringLogicType(LogicType l){
    string s;
    if(l == And){ s = " & "; }
    else{ s = " | "; }
    return s;
}

string StringOPType(OPType l){
    string s;
    if(l == Plus){ s = "+"; }
    else if(l == Minus){ s = "-"; }
    else if(l == Multi){ s = "*"; }
    else if(l == Divide){ s = "/"; }
    else { }
    return s;
}
string StringExpr(Expr* e){
    string s;
    if(typeid(*e) == typeid(IntExpr)){
        s = Int2String(((IntExpr*)e)->i);
    }
    else if(typeid(*e) == typeid(VarExpr)){
        s = ((VarExpr*)e)->x;
    }
    else /*if(typeid(*e) == typeid(ArrayExpr)){
        s = ((ArrayExpr*)e)->n;
        s = s + "[ ";
        s = s + StringExpr(((ArrayExpr*)e)->e);
        s = s + " ]";
    }
    else */if(typeid(*e) == typeid(BinExpr)){
        s = StringExpr(((BinExpr*)e)->e1)+StringOPType(((BinExpr*)e)->op)+StringExpr(((BinExpr*)e)->e2);
    }
    else{
    }
    return s;
}
string Prop_to_String(Prop* p){
    string s;
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){ s = "(true)"; }
        else{ s = "(false)"; }
    }
    else if(typeid(*p) == typeid(NegProp)){
        s = "~(" + Prop_to_String(((NegProp*)p)->p)+")";
    }
    else if(typeid(*p) == typeid(BinProp)){
        s = Prop_to_String(((BinProp*)p)->p1)+StringLogicType(((BinProp*)p)->l)+Prop_to_String(((BinProp*)p)->p2);
    }
    else if(typeid(*p) == typeid(InequProp)){
        if(((InequProp*)p)->p == LT){
            s = StringExpr(((InequProp*)p)->e1)+string("<")+StringExpr(((InequProp*)p)->e2);
        }
        else if(((InequProp*)p)->p == GT){
        	s = StringExpr(((InequProp*)p)->e1)+string(">")+StringExpr(((InequProp*)p)->e2);
        }
        else{
        	s = StringExpr(((InequProp*)p)->e1)+string("=")+StringExpr(((InequProp*)p)->e2);
        }
    }
    else{
        s = "error";
    }
    return s;
}

bool CompareExpr(Expr *e1, Expr *e2){
    bool r = true;
    if(typeid(*e1) == typeid(IntExpr)){
        if(typeid(*e2) == typeid(IntExpr)){
            if(((IntExpr*)e2)->i == ((IntExpr*)e1)->i){
                r = true; return r;
            }
            else{
                r = false; return r;
            }
        }
        else{
            r = false; return r;
        }
    }
    else if(typeid(*e1) == typeid(SelectExpr)){
        if(typeid(*e2) == typeid(SelectExpr)){
            if(CompareExpr(((SelectExpr*)e2)->a, ((SelectExpr*)e1)->a) == 0){
                if(CompareExpr((SelectExpr*)e2, (SelectExpr*)e1) == 0){
                    r = true;
                    return r;
                }
                else{
                    r = false;
                    return r;
                }
            }
            else{
                r = false;
                return r;
            }
        }
        else{
            r = false;
            return r;
        }
    }
    else if(typeid(*e1) == typeid(VarExpr)){
        if(typeid(*e2) == typeid(VarExpr)){
            if(strcmp(((VarExpr*)e1)->x, ((VarExpr*)e2)->x) == 0){
                r = true; return r;
            }
            else{
                r = false; return r;
            }
        }
        else{
            r = false; return r;
        }
    }
    else if(typeid(*e1) == typeid(BinExpr)){
        if(typeid(*e2) == typeid(BinExpr)){
            r = CompareExpr(((BinExpr*)e1)->e1, ((BinExpr*)e2)->e1) | CompareExpr(((BinExpr*)e1)->e2, ((BinExpr*)e2)->e2);
            return r;
        }
        else{
            r = false;
            return r;
        }
    }
    else{
    }
    return r;
}
